Fix msg.value balance accounting in invariant tests - #590

Summary

• generate symbolic msg.value only for payable invariant targets
• apply funded top-level CALL value transfers to sender and recipient balances
• preserve self-transfer semantics and discard solver-proven underfunded states
• restore persistent state and transaction-start transient storage after any EVM failure
• add unit and invariant regressions for transfer, rollback, and positive-value reachability

Validation

• git diff --check
• independent static review with gpt-5.6-sol via the non-cyber codex-lb route

Tests were not run because this review was constrained to passive/static inspection and prohibited executing repository code, builds, package managers, or hooks.